This Open Access book presents the results of the "Collaborative Embedded Systems" (CrESt) project, aimed at adapting and complementing the methodology underlying modeling techniques developed to cope with the challenges of the dynamic structures of collaborative embedded systems (CESs) based on the SPES development methodology. In order to manage the high complexity of the individual systems and the dynamically formed interaction structures at runtime, advanced and powerful development methods are required that extend the current state of the art in the development of embedded systems and cyber-physical systems. The methodological contributions of the project support the effective and efficient development of CESs in dynamic and uncertain contexts, with special emphasis on the reliability and variability of individual systems and the creation of networks of such systems at runtime. The project was funded by the German Federal Ministry of Education and Research (BMBF), and the case studies are therefore selected from areas that are highly relevant for Germany's economy (automotive, industrial production, power generation, and robotics). It also supports the digitalization of complex and transformable industrial plants in the context of the German government's "Industry 4.0" initiative, and the project results provide a solid foundation for implementing the German government's high-tech strategy "Innovations for Germany" in the coming years.

Softwareentwicklung erfordert – ausgehend von informellen Problemstellungen – Spezifikationen unter Festlegung der Daten- und Rechenstrukturen, Implementierungen und die Verifikation der Korrektheit. Zur Bewältigung dieser Aufgaben hat die Informatik eine Reihe grundlegender Ansätze und Methoden entwickelt, die in zwei Bänden in einem einheitlichen Rahmen zusammengefasst und an Beispielen erläutert werden. Der erste Band widmet sich der Spezifikationen von Daten- und Rechenstrukturen, der Spezifikation und Implementierung sowie dem Nachweis der Korrektheit funktionaler, prozeduraler und objektorientierter Programme. Der zweite Band dieses umfassenden und zugleich grundlagenorientierten Werkes behandelt softwareintensive Systeme und ihre Darstellung durch Zustandsmaschinen, nebenläufige Programme mit gemeinsamen Variablen, Datenflussprogramme, Schnittstellspezifikation, Zeitfluss, Architektur verteilter Systeme, Prozessmodellierung, Verfeinerung und spezifische Formalismen wie CSP, TLA und prädikative Spezifikation.Dies schließt unter anderem auch Themen wie Korrektheitsbeweise in Hinblick auf Sicherheit und Lebendigkeit sowie schrittweise Verfeinerung ein. Insbesondere werden im Buch die Grundlagen für eine wissenschaftlich abgesicherte Entwicklung von Programmen gelegt.

This book provides a comprehensive introduction into the SPES XT modeling framework. Moreover, it shows the applicability of the framework for the development of embedded systems in different industry domains and reports on the lessons learned. It also describes how the SPES XT modeling framework can be tailored to meet domain and project-specific needs. The book is structured into four parts: Part I "Starting Situation" discusses the status quo of the development of embedded systems with specific focus on model-based engineering and summarizes key challenges emerging from industrial practice. Part II "Modeling Theory" introduces the SPES XT modeling framework and explains the core underlying principles. Part III "Application of the SPES XT Framework" describes the application of the SPES XT modeling framework and how it addresses major industrial challenges. Part IV "Evaluation and Technology Transfer" assess the impact of the SPES XT modeling framework and includes various exemplary applications from automation, automotive, and avionics. Overall, the SPES XT modeling framework offers a seamless model-based engineering approach. It addresses core challenges faced during the engineering of embedded systems. Among others, it offers aligned and integrated techniques for the early validation of engineering artefacts (including requirements and functional and technical designs), the management of product variants and their variability, modular safety assurance and deployment of embedded software.

A lucid statement of the philosophy of modular programming can be found in a 1970 textbook on the design of system programs by Gouthier and Pont [1, l Cfl0. 23], which we quote below: A well-defined segmentation of the project effort ensures system modularity. Each task fonos a separate, distinct program module. At implementation time each module and its inputs and outputs are well-defined, there is no confusion in the intended interface with other system modules. At checkout time the in tegrity of the module is tested independently; there are few sche duling problems in synchronizing the completion of several tasks before checkout can begin. Finally, the system is maintained in modular fashion; system errors and deficiencies can be traced to specific system modules, thus limiting the scope of detailed error searching. Usually nothing is said about the criteria to be used in dividing the system into modules. This paper will discuss that issue and, by means of examples, suggest some criteria which can be used in decomposing a system into modules. A Brief Status Report The major advancement in the area of modular programming has been the development of coding techniques and assemblers which (1) allow one modu1e to be written with little knowledge of the code in another module, and (2) alJow modules to be reas sembled and replaced without reassembly of the whole system.

A mathematical and logical foundation for the specification and development of interactive systems based on a model that describes systems in terms of their input/output behavior. Based on this model, the authors build a basic method, called FOCUS, that enables interactive systems to be described by characterizing their histories of message interaction. The book progresses from an introduction and guided tour of FOCUS through streams, specifications and their properties, and behavioral, interface, and conditional refinements.

In computing science design plays an eminently important role. By now, it is quite clear that the issue of proper design of programs within a formal calculus is one of the most interesting and most difficult parts of computing science. Many demanding problems have to be envisaged here such as notations, rules and calculi, and the study of semantic models. We are 'far away from comprehensive and widely accepted solutions in these areas. Discussions at the summer school have clearly shown that people have quite different perspectives and priorities with respect to these three main areas. There is a general agreement that notation is very important. Here, notation is not so much used in the sense of "syntactic sugar," but rather in the sense of abstract syntax, in the sense of language constructs. Proper notation can significantly improve our understanding of the nature of the objects that we are dealing with and simplify the formal manipulation of these objects. However, influenced by educational background, habits, and schools of thought there are quite different tastes with respect to notation. The papers in these proceedings show very clearly how different those notations can be even when talking about quite similar objects.

Embedded systems have long become essential in application areas in which human control is impossible or infeasible. The development of modern embedded systems is becoming increasingly difficult and challenging because of their overall system complexity, their tighter and cross-functional integration, the increasing requirements concerning safety and real-time behavior, and the need to reduce development and operation costs. This book provides a comprehensive overview of the Software Platform Embedded Systems (SPES) modeling framework and demonstrates its applicability in embedded system development in various industry domains such as automation, automotive, avionics, energy, and healthcare. In SPES 2020, twenty-one partners from academia and industry have joined forces in order to develop and evaluate in different industrial domains a modeling framework that reflects the current state of the art in embedded systems engineering. The content of this book is structured in four parts. Part I "Starting Point" discusses the status quo of embedded systems development and model-based engineering, and summarizes the key requirements faced when developing embedded systems in different application domains. Part II "The SPES Modeling Framework" describes the SPES modeling framework. Part III "Application and Evaluation of the SPES Modeling Framework" reports on the validation steps taken to ensure that the framework met the requirements discussed in Part I. Finally, Part IV "Impact of the SPES Modeling Framework" summarizes the results achieved and provides an outlook on future work. The book is mainly aimed at professionals and practitioners who deal with the development of embedded systems on a daily basis. Researchers in academia and industry may use it as a compendium for the requirements and state-of-the-art solution concepts for embedded systems development.

The Summer School in Marktoberdorf 1990 had as its overall theme the development of programs as an activity that can be carried out based on and supported by a mathematical method. In particular mathematical methods for the development of programs as parts of distributed systems were included. Mathematical programming methods are a very important topic for which a lot of research in recent years has been carried out. In the Marktoberdorf Summer School outstanding scientists lectured on mathematical programming methods. The lectures centred around logical and functional calculi for the * specification, * refinement, * verification of programs and program systems. Some extremely remarkable examples were given. Looking at these examples it becomes clear that proper research and teaching in the area of program methodology should always show its value by being applied at least to small examples or case studies. It is one of the problems of computing science that examples and case studies have to be short and small to be lJresentable in lectures and papers of moderate size. However, even small examples can tell a lot about the tractability and adequacy of methods and being able to treat small examples does at least prove that the method can be applied in modest ways. Furthermore it demonstrates to some extent the notational and calculational overhead of applying formal methods.

Computing Science is a science of constructive methods. The solution of a problem has to be described formally by constructive techniques, if it is to be evaluated on a computer. The Marktoberdorf Advanced Study Institute 1988 presented a comprehensive survey of the recent research in constructive methods in Computing Science. Some approaches to a methodological framework and to supporting tools for specification, development and verification of software systems were discussed in detail. Other lectures dealt with the relevance of the foundations of logic for questions of program construction and with new programming paradigms and formalisms which have proven to be useful for a constructive approach to software development. The construction, specification, design and verification especially of distributed and communicating systems was discussed in a number of complementary lectures. Examples for those approaches were given on several levels such as semaphores, nondeterministic state transition systems with fairness assumptions, decomposition of specifications for concurrent systems in liveness and safety properties and functional specifications of distributed systems. Construction methods in programming that were presented range from type theory, the theory of evidence, theorem provers for proving properties of functional programs to category theory as an abstract and general concept for the description of programming paradigms.

Modern information processing systems show such complex properties as distribution, parallelism, interaction, time dependency, and nondeterminism. For critical applications, mathematical methods are needed to model the systems and to support their development and validation. Impressive progress in mathematical methods for programming software systems makes it possible to think about unifying the different approaches. This book gives a comprehensive overview of existing methods and presents some of the most recent results in applying them. The main topics are: advanced programming techniques, foundations of systems engineering, mathematical support methods, and application of the methods. The approaches presented are illustrated by examples and related to other approaches.

Advanced research on the description of distributed systems and on design calculi for software and hardware is presented in this volume. Distinguished researchers give an overview of the latest state of the art.

The development of information processing systems requires models, calculi, and theories for the analysis of computations. It is well understood by now that more complex software systems cannot and should not be constructed in one step. A careful, systematic, and disciplined structuring of the development process is most adequate. It should start from basic requirement specifications in which aU the relevant details of the problem to be solved are formalized. The envisaged solution should be developed step by step by adding more and more details and giving evidence-in the best case by formal proof-to show the correctness of the developed steps. The development ends if a description of a solution is obtained that has aU the required properties. The Summer School in Marktoberdorf 1992 showed significant approaches in this area to refinement calculi, to models of computation, and as a special issue to the treatment of reactive timed systems. Like in the many summer schools before, the success of the 1992 Summer School was not only due to the excellent lectures, but even more due to the brilliant students taking part in the discussions at the summer school, the exchange of different views, and the recognition of the similarity of a number of different view points. These were some of the most important contributions of the summer school. fu the following the proceedings of the summer school are collected. They show the maturity of the field in an impressive way.

Software development for the automotive domain has become the enabling te- nologyforalmostallsafety-criticalandcomfortfunctionso?eredtothecustomer. Ninety percentofallinnovations inautomotive systems aredirectly or indirectly enabled by embedded software. The numbers of serious accidents have declined in recent years, despite constantly increasing tra?c; this is correlated with the introduction of advanced, software-enabled functionality for driver assistance, such as electronic stability control. Software contributes signi?cantly to the - tomotive value chain. By 2010 it is estimated that software will make up 40% of the value creation of automotive electrics/electronics. However, with the large number of software-enabled functions, their int- actions, and the corresponding networking and operating infrastructure, come signi?cant complexities both during the automotive systems engineering p- cess and at runtime. A central challenge for automotive systems development is the scattering of functionality across multiple subsystems, such as electronic control units (ECUs) and the associated networks. As an example, consider the central locking systems (CLS), whose functionality is spread out over up to 19 di?erent ECUs in some luxury cars. Of course, this includes advanced functi- ality, such as seat positioning and radio tuning according to driver presets upon entry, as well as unlocking in case of a detected impact or accident. However, thisexampledemonstratesthatmodernautomotivesystemsbridgecomfort-and safety-critical functionality. This induces particular demands on safety and - curity, and, in general, software and systems quality. The resulting challenges and opportunities were discussed, in depth, at the second Automotive Software Workshop San Diego (ASWSD) 2006, on whose results we report here.

This book constitutes the thoroughly refereed post-proceedings of the First Automotive Software Workshop, ASWD 2004, held in San Diego, CA, USA in January 2004. The 10 revised full papers presented were carefully reviewed and selected from 26 lectures held at the workshop that brought together experts from industry and academia, working on highly complex, distributed, reactive software systems related to the automotive domain.

Software engineering has over the years been applied in many different fields, ranging from telecommunications to embedded systems in car and aircraft industry as well as in production engineering and computer networks. Foundations in software technology lie in models allowing to capture application domains, detailed requirements, but also to understand the structure and working of software systems like software architectures and programs. These models have to be expressed in techniques based on discrete mathematics, algebra and logics. However, according to the very specific needs in applications of software technology, formal methods have to serve the needs and the quality of advanced software engineering methods, especially taking into account security aspects in Information Technology. This book presents mathematical foundations of software engineering and state-of-the-art engineering methods in their theoretical substance in the step towards practical applications to examine software engineering techniques and foundations used for industrial tasks.

The contributions in this volume emerged from lectures of the 25th International Summer School on Engineering Theories of Software Intensive Systems, held at Marktoberdorf, Germany from August 3 to August 15, 2004.

Testing is the primary hardware and software verification technique used by industry today. Usually, it is ad hoc, error prone, and very expensive. In recent years, however, many attempts have been made to develop more sophisticated formal testing methods. This coherent book provides an in-depth assessment of this emerging field, focusing on formal testing of reactive systems.

This book is based on a seminar held in Dagstuhl Castle, Germany, in January 2004. It presents 19 carefully reviewed and revised lectures given at the seminar in a well-balanced way ensuring competent complementary coverage of all relevant aspects. An appendix provides a glossary for model-based testing and basics on finite state machines and on labelled transition systems. The lectures are presented in topical sections on testing of finite state machines, testing of labelled transition systems, model-based test case generation, tools and case studies, standardized test notation and execution architectures, and beyond testing.

Thevolumecomprises?nalversionsofthepaperspresentedatthe5thInternat- nal Andrei Ershov Memorial Conference "Perspectives of System Informatics," Akademgorodok (Novosibirsk, Russia), July 9-12, 2003. The main goal of the conference was to give an overview of research directions that are decisive for growth in the major areas of research activities in system informatics. The conference was held to honor the 70th anniversary of Ershov's closest colleague, the late Prof. Igor Pottosin (1933-2001), and his outstanding cont- bution towards advancing informatics. The ?rst four Andrei Ershov conferences were held in May 1991, June 1996, July 1999, and July 2001, and they proved to be signi?cant international events. Andrei Ershov was one of the early Russian pioneers in the ?eld of theo- tical and systems programming, a founder of the Siberian School of Computer Science. His closest colleague, Igor Pottosin, worked for the Siberian Branch of the Russian Academy of Sciences from 1958, step by step ?lling positions from junior researcher to director of the A.P. Ershov Institute of Informatics - stems. In later years he headed the Laboratory of Systems Programming in this institute and the Department of Programming at Novosibirsk State University.

Das Buch behandelt Prinzipien und Methoden der Software-Entwicklung fA1/4r Kommunikationsnetze, basierend auf praktischen Erfahrungen aus einer Reihe von Software-Projekten. Die spezifischen Merkmale dieser Software sind parallele AblAufe, zeitkritisches Antwortverhalten, komplexe FunktionalitAt und sehr hohe QualitAtsanforderungen. Eine wesentliche Rolle bei der Beherrschung der Software-KomplexitAt spielt die Architektur. Sie stellt die Regeln und Methoden fA1/4r einen effektiven Systementwurf zur VerfA1/4gung, auf dem sich der gesamte Entwicklungsprozess abstA1/4tzen kann. Dazu gehArt eine vollstAndige Spezifikationsmethodik auf der Grundlage einer formalen Sprache, deren Semantik an den typischen Merkmalen von Kommunikations-Software ausgerichtet ist. Schwerpunkt der AusfA1/4hrungen ist die Anpassung der Software-Entwicklung an die steigenden Anforderungen bezA1/4glich FunktionalitAt, Marktorientierung, Kosten und Zeit.

This book constitutes the thoroughly refereed post-proceedings of the 4th International Andrei Ershov Memorial Conference, PSI 2001, held in Akademgorodok, Novosibirsk, Russia, in July 2001.The 50 revised papers presented together with 2 invited memorial papers devoted to the work of Andrei Ershov were carefully selected during 2 rounds of reviewing and improvement. The book offers topical sections on computing and algorithms, logical methods, verification, program transformation and synthesis, semantics and types, processes and concurrency, UML specification, Petri nets, testing, software construction, data and knowledge bases, logic programming, constraint programming, program analysis, and language implementation.

Today's distributed systems are characterized by interactions-often complex-between many different hardware and software components cooperating and exchanging information. To simplify development of interactive systems and facilitate communication and documentation, experts of varying disciplines employ descriptions, or specifications, of a given system's behavior and/or structure. Specification and Development of Interactive Systems offers a unique approach to program and software development suitable for large distributed systems, with an emphasis on modular system development and systems engineering. The authors build a basic method, called FOCUS, that enables interactive systems to be described by characterizing their histories of message interaction. The method covers functional requirements, timing, structure, and implementation issues of systems. In addition, the book describes how to connect the models and techniques to tables and diagram-based methods popular in practical systems engineering. Topics and features: * Specification of interface behavior and modular top-down system development * Specification of time and the modeling of hardware/software systems * Interface refinement and the modeling of development steps leading from one level of abstraction to the next * State transition diagrams and tables and the usage of common description techniques, such as found in UML This book provides a mathematical and logical foundation for the specification and development of interactive systems based on a model that describes systems in terms of their input/output behavior. The reader gains a comprehensive understanding of all fundamental models, techniques, and methods for interactive system design. The book is an essential resource for all researchers and professionals in computer science, software systems engineering and computer engineering.

This volume comprises the papers presented at the Third International Andrei Ershov Memorial Conference \Perspectives of System Informatics", Akadem- rodok (Novosibirsk, Russia), July 6{9, 1999. The main goal of the conference was to give an overview of research directions which are decisive for the growth of major areas of research activities in system informatics. The conference was the third one in the line. The r st and second inter- tionalconferences\PerspectivesofSystemInformatics"wereheldinNovosibirsk, Akademgorodok, in May, 1991, and June, 1996, respectively. Both conferences gathered a wide spectrum of specialists and were undoubtedly very successful. The third conferenceincluded many of the subjects of the second conference, such as theoretical computer science, programming methodology, new infor- tiontechnologies,andthepromising eldofarti cialintelligence|asimportant components of system informatics. The style of the second conference was p- served to a certain extent in that there were a considerable number of invited papers in addition to the contributed papers. However,posters were replaced by short talks mainly given by young researchers.

This book constitutes the refereed post-conference proceedings of the Second International Andrei Ershov Memorial Conference on System Informatics, held in Akademgorodok, Novosibirsk, Russia, in June 1996.
The 27 revised full papers presented together with 9 invited contributions were thoroughly refereed for inclusion in this volume. The book is divided in topical sections on programming methodology, artificial intelligence, natural language processing, machine learning, dataflow and concurrency models, parallel programming, supercompilation, partial evaluation, object-oriented programming, semantics and abstract interpretation, programming and graphical interfaces, and logic programming.

The RPC-memory specification problem was proposed by Broy and Lamport as a case study in the formal design of distributed and concurrent systems. As a realistic example typical for operating systems and hardware design, the RPC-memory problem was used as the basis for comparing various approaches to formal specification, refinement, and verification.
Preliminary solutions were discussed during a workshop at Schloss Dagstuhl, Germany, in September 1994. Then an extensive discussion took place between the referees and authors. Finally 15 thoroughly revised papers were accepted for inclusion in this volume in full detail together with the problem statement and a synopsis.

Advanced research on the description of distributed systems and on design calculi for software and hardware is presented in this volume. Distinguished researchers give an overview of the latest state of the art.